package at.tasat.solver;

import java.util.Collection;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;
import java.util.Stack;

import at.tasat.assignment.PartialAssignment;
import at.tasat.cnf.Clause;
import at.tasat.cnf.Cnf;
import at.tasat.cnf.Literal;
import at.tasat.solver.ThreadManager.ManagedThread;
import at.tasat.util.IntSet;
import at.tasat.util.IntStack;

public final class Solver {
	public static Solver create(Cnf cnf) {
		return create(new SolverConfiguration(), cnf);
	}

	public static Solver create(SolverConfiguration config, Cnf cnf) {
		PartialAssignment assignment = new PartialAssignment(cnf.getNumberOfVariables());
		VariableOccurencesList occurencesList = createOccurencesList(cnf, assignment);
		Queue variablesToAssign = createVariablesQueue(config.getQueueFactory(), cnf, assignment, occurencesList);
		Stack<Collection<Clause>> removedClauses = new Stack<Collection<Clause>>();
		return new Solver(config, cnf, new ThreadManager((config.getMaxThreads() - 1) * 2), assignment, occurencesList, variablesToAssign, removedClauses);
	}

	private final SolverConfiguration config;
	private final Cnf cnf;
	private final ThreadManager threadManager;
	private final PartialAssignment assignment;
	private final VariableOccurencesList occurencesList;
	private final Queue variablesToAssign;
	private final Stack<Collection<Clause>> removedClauses;

	private Solver(SolverConfiguration config, Cnf cnf, ThreadManager manager, PartialAssignment assignment, VariableOccurencesList occurencesList, Queue variablesToAssign,
			Stack<Collection<Clause>> removedClauses) {
		this.config = config;
		this.cnf = cnf;
		this.threadManager = manager;
		this.assignment = assignment;
		this.occurencesList = occurencesList;
		this.variablesToAssign = variablesToAssign;
		this.removedClauses = removedClauses;
	}

	public void releaseThreadManager() {
		threadManager.release();
	}

	private static VariableOccurencesList createOccurencesList(Cnf cnf, PartialAssignment assignment) {
		VariableOccurencesList occurencesList = new VariableOccurencesList(cnf.getNumberOfVariables());
		for (Clause clause : cnf) {
			for (int i = 0; i < clause.getNumberOfLiterals(); i++) {
				int variableId = Literal.getVariableId(clause.getLiteral(i));
				VariableOccurences occurences = occurencesList.getOccurences(variableId);
				if (!assignment.isSatisfied(clause)) {
					occurences.addClause(clause);
				}
			}
		}
		return occurencesList;
	}

	private static Queue createVariablesQueue(QueueFactory factory, Cnf cnf, PartialAssignment assignment, VariableOccurencesList occurencesList) {
		Queue variablesToAssign = factory.create(cnf.getNumberOfVariables(), occurencesList);
		for (int variableId = 1; variableId <= cnf.getNumberOfVariables(); variableId++) {
			if (!assignment.isAssigned(variableId)) {
				variablesToAssign.enqueue(variableId);
			}
		}
		return variablesToAssign;
	}

	public boolean solve() throws InterruptedException, SolverException {
		return solve(0, getMaxNumberOfSteps(cnf.getNumberOfVariables()));
	}

	private boolean solve(long nSteps, long nMaxSteps) throws InterruptedException, SolverException {
		final Thread thread = Thread.currentThread();
		int variableId = 0;
		boolean phase = false;
		ManagedThread[] threads = null;

		int state = 1;
		final IntStack states = new IntStack(cnf.getNumberOfVariables() + 1 - assignment.getNumberOfAssignments());
		final IntStack literals = new IntStack(cnf.getNumberOfVariables() + 1 - assignment.getNumberOfAssignments());
		states.push(0);
		literals.push(0);
		boolean sat = false;
		try {
			while (state != 0) {
				if (thread.isInterrupted()) {
					throw new InterruptedException();
				}
				assert states.size() - 1 <= cnf.getNumberOfVariables();
				assert literals.size() <= states.size();
				assert variablesToAssign.size() <= cnf.getNumberOfVariables();
				assert assignment.getNumberOfAssignments() <= cnf.getNumberOfVariables();
				assert nSteps < nMaxSteps;
				sat = false;
				switch (state) {
				case 1: // propagate units
					boolean conflictFound = !propagateUnits();
					assert conflictFound == isAnyClauseUnsatisfied(cnf);
					// assert 0 <= (nSteps = nSteps +
					// getMaxNumberOfSteps(assignment.getNumberOfAssignments() -
					// nPrevAssignments));
					sat = !conflictFound;
					state = conflictFound ? 9 : 2;
					break;
				case 2: // assign pure literals
					assignPureLiterals();
					// assert 0 <= (nSteps = nSteps +
					// getMaxNumberOfSteps(assignment.getNumberOfAssignments() -
					// nPrevAssignments));
					sat = areAllClausesSatisfied();
					state = sat ? 0 : 3;
					break;
				case 3: // decide on next decision variable
					assert variablesToAssign.size() > 0;
					variableId = variablesToAssign.peek();
					threads = threadManager.fork(2);
					state = threads != null ? 11 : 4;
					break;
				case 4: // decide variable = true, try solve
					phase = occurencesList.getOccurences(variableId).getDominantPhase();
					doDecision(variableId, phase);
					nSteps++;
					states.push(5);
					state = 10;
					break;
				case 5: // undo decision
					undoDecision(variableId);
					state = 6;
					break;
				case 6: // decide variable = false, try solve
					phase = !phase;
					doDecision(variableId, phase);
					nSteps++;
					states.push(7);
					state = 10;
					break;
				case 7: // undo decision
					undoDecision(variableId);
					state = 8;
					break;
				case 8: // solving failed
					sat = false;
					state = 9;
					break;
				case 9: // end recursion
					int literal = literals.pop();
					variableId = Literal.getVariableId(literal);
					phase = Literal.getPhase(literal);
					state = states.pop();
					break;
				case 10: // start recursion
					literals.push(Literal.toLiteral(variableId, phase));
					state = 1;
					break;
				case 11:
					sat = forkAndSolve(threads, variableId, nSteps, nMaxSteps);
					state = sat ? 0 : 9;
					break;
				default:
					assert false;
				}
			}
		} catch (InterruptedException ie) {
			throw ie;
		} catch (Throwable t) {
			throw new SolverException(t, state, states);
		}
		// assert sat || nSteps == maxSteps

		assert sat == areAllClausesSatisfied();
		return sat;
	}

	private boolean forkAndSolve(ManagedThread[] threads, int variableId, long nSteps, long nMaxSteps) throws InterruptedException {
		boolean sat;
		Object monitor = new Object();
		MyRunnable positiveRunnable = new MyRunnable(monitor, this, variableId, true, nSteps, nMaxSteps);
		MyRunnable negativeRunnable = new MyRunnable(monitor, this, variableId, false, nSteps, nMaxSteps);
		ManagedThread positiveThread = threads[0];
		ManagedThread negativeThread = threads[1];
		try {
			sat = false;
			synchronized (monitor) {
				positiveThread.start(positiveRunnable);
				negativeThread.start(negativeRunnable);
				do {
					if (Thread.interrupted()) {
						throw new InterruptedException();
					}
					monitor.wait();
					if (positiveRunnable.hasFailed()) {
						throw new RuntimeException(positiveRunnable.getException());
					}
					if (negativeRunnable.hasFailed()) {
						throw new RuntimeException(negativeRunnable.getException());
					}
					sat = positiveRunnable.getResult() || negativeRunnable.getResult();
				} while (!sat && (!positiveRunnable.isFinished() || !negativeRunnable.isFinished()));
			}
			if (sat) {
				PartialAssignment solution = (positiveRunnable.getResult() ? positiveRunnable : negativeRunnable).solver.getAssignment();
				solution.copyTo(assignment);
			}
		} finally {
			positiveThread.interrupt(positiveRunnable);
			negativeThread.interrupt(negativeRunnable);
		}
		return sat;
	}

	private boolean propagateUnits() {
		HashSet<Clause> touchedByIteration = new HashSet<Clause>();
		for (IntSet unitLiterals = getUnitLiterals(cnf); unitLiterals.size() > 0; unitLiterals = getUnitLiterals(touchedByIteration)) {
			touchedByIteration.clear();
			for (int literal : unitLiterals) {
				int variableId = Literal.getVariableId(literal);
				if (assignment.isAssigned(variableId)) {
					assert !assignment.getAssignmentOfVariable(variableId).isTrue(literal);
					return false;
				}
				boolean value = Literal.getPhase(literal);
				VariableOccurences occurences = occurencesList.getOccurences(variableId);
				makeAssignment(variableId, value, false);
				Iterator<Clause> touchedByCurrentLiteral = occurences.getOccurences(!value);
				while (touchedByCurrentLiteral.hasNext()) {
					Clause clause = touchedByCurrentLiteral.next();
					if (assignment.isUnsatisfied(clause)) {
						return false;
					} else if (!assignment.isSatisfied(clause)) {
						touchedByIteration.add(clause);
					}
				}
			}
		}
		return true;
	}

	private IntSet getUnitLiterals(Cnf clauses) {
		IntSet unitLiterals = new IntSet(-cnf.getNumberOfVariables(), cnf.getNumberOfVariables());
		for (Clause clause : clauses) {
			int unitVariableId = assignment.getUnitVariableId(clause);
			if (unitVariableId != 0) {
				int literal = clause.getLiteralOfVariable(unitVariableId);
				unitLiterals.put(literal);
			}
		}
		return unitLiterals;
	}

	private IntSet getUnitLiterals(HashSet<Clause> clauses) {
		IntSet unitLiterals = new IntSet(-cnf.getNumberOfVariables(), cnf.getNumberOfVariables());
		for (Clause clause : clauses) {
			int unitVariableId = assignment.getUnitVariableId(clause);
			if (unitVariableId != 0) {
				int literal = clause.getLiteralOfVariable(unitVariableId);
				unitLiterals.put(literal);
			}
		}
		return unitLiterals;
	}

	private boolean isAnyClauseUnsatisfied(Iterable<Clause> clauses) {
		for (Clause clause : clauses) {
			if (assignment.isUnsatisfied(clause)) {
				return true;
			}
		}
		return false;
	}

	private void assignPureLiterals() {
		for (int variableId = 1; variableId <= cnf.getNumberOfVariables(); variableId++) {
			if (!assignment.isAssigned(variableId)) {
				VariableOccurences occurences = occurencesList.getOccurences(variableId);
				if (occurences.isPurePositive()) {
					makeAssignment(variableId, true, false);
				} else if (occurences.isPureNegative()) {
					makeAssignment(variableId, false, false);
				}
			}
		}
	}

	private boolean areAllClausesSatisfied() {
		for (Clause clause : cnf) {
			if (!assignment.isSatisfied(clause)) {
				return false;
			}
		}
		return true;
	}

	private void doDecision(int variableId, boolean phase) {
		makeAssignment(variableId, phase, true);
	}

	private void undoDecision(int decisionVariableId) {
		int variableId = 0;
		int nAssignments = assignment.getNumberOfCurrentDecisionAssignments();
		for (int i = 0; i < nAssignments; i++) {
			variableId = assignment.popAssignment();
			assert !variablesToAssign.contains(variableId);
			variablesToAssign.reenqueue(variableId);
			VariableOccurences occurences = occurencesList.getOccurences(variableId);
			occurences.addClauses(removedClauses.pop());
		}
		assert variableId == decisionVariableId;
	}

	private void makeAssignment(int variableId, boolean phase, boolean isDecision) {
		assert variablesToAssign.contains(variableId);
		variablesToAssign.remove(variableId);
		assignment.pushAssignment(variableId, phase, isDecision);
		VariableOccurences occurences = occurencesList.getOccurences(variableId);
		Set<Clause> clausesToRemove = occurences.removeOccurences(phase);
		assert allSatisfied(clausesToRemove);
		removedClauses.push(clausesToRemove);
	}

	private boolean allSatisfied(Set<Clause> clauses) {
		for (Clause clause : clauses) {
			if (!assignment.isSatisfied(clause)) {
				return false;
			}
		}
		return true;
	}

	private static long getMaxNumberOfSteps(int nVariables) {
		return (long) Math.pow(2, nVariables + 1) - 2;
	}

	public PartialAssignment getAssignment() {
		return assignment;
	}

	@Override
	public String toString() {
		return assignment.toString();
	}

	private static class MyRunnable implements Runnable {

		private final Object monitor;
		private final Solver solver;
		private final long nSteps;
		private final long nMaxSteps;
		private Boolean sat;
		private SolverException exception;

		public MyRunnable(Object monitor, Solver solver, int variableId, boolean phase, long nSteps, long nMaxSteps) {
			PartialAssignment assignment = solver.assignment.clone();
			VariableOccurencesList occurencesList = solver.occurencesList.clone();
			Queue variablesToAssign = solver.config.getQueueFactory().clone(solver.variablesToAssign, occurencesList);
			Stack<Collection<Clause>> removedClauses = new Stack<Collection<Clause>>();

			this.monitor = monitor;
			this.solver = new Solver(solver.config, solver.cnf, solver.threadManager, assignment, occurencesList, variablesToAssign, removedClauses);
			this.solver.doDecision(variableId, phase);
			this.nSteps = nSteps + 1;
			this.nMaxSteps = nMaxSteps;
			sat = null;
			exception = null;
		}

		public boolean isFinished() {
			return sat != null || exception != null;
		}

		public boolean hasFailed() {
			return exception != null;
		}

		public Exception getException() {
			return exception;
		}

		public boolean getResult() {
			return sat != null ? sat : false;
		}

		@Override
		public void run() {
			try {
				sat = solver.solve(nSteps, nMaxSteps);
			} catch (InterruptedException ie) {
				sat = null;
			} catch (SolverException se) {
				exception = se;
			} finally {
				synchronized (monitor) {
					monitor.notifyAll();
				}
			}
		}

	}
}
